Termination w.r.t. Q proof of TRS/higher-order/AotoYam028.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(consif, true), x), ys) → app(app(cons, x), ys)
app(app(app(consif, false), x), ys) → ys
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(consif, app(f, x)), x), app(app(filter, f), xs))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(consif, true), x), ys) → app(app(cons, x), ys)
app(app(app(consif, false), x), ys) → ys
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(consif, app(f, x)), x), app(app(filter, f), xs))

Q is empty.